\begin{tabbing}
$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), ${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type).
\\[0ex]trivial{-}component($f$) $\mid${-} ${\it es}$,${\it in}$,${\it out}$.$\exists$\=$g$:E(${\it out}$)$\rightarrow$E(${\it in}$)\+
\\[0ex](($\forall$$e$:E(${\it out}$). $g$($e$) c$\leq$ $e$ \& ${\it out}$($e$) = $f$(${\it in}$($g$($e$))) $\in$ $B$)
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E(${\it out}$). ($e$ $<$ ${\it e'}$) $\Leftarrow\!\Rightarrow$ ($g$($e$) $<$ $g$(${\it e'}$))))
\-
\end{tabbing}